$\forall$${\it es}$:ES, $i$:Id, $L$:Knd List, $x$:Id, $T$:Type. es{-}frame(${\it es}$;$i$;$L$;$x$;$T$) $\in$ Prop